Skip to content

[Merged by Bors] - feat(Topology/Connected): connected and path components of products and pi types - #41661

Closed
korbonits wants to merge 2 commits into
leanprover-community:masterfrom
korbonits:path-component-prod-pi
Closed

[Merged by Bors] - feat(Topology/Connected): connected and path components of products and pi types#41661
korbonits wants to merge 2 commits into
leanprover-community:masterfrom
korbonits:path-component-prod-pi

Conversation

@korbonits

@korbonits korbonits commented Jul 12, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Add connectedComponent_prod/pi and pathComponent_prod/pi: the (path) component of a point in a product is the product of the components of its coordinates. Also add the missing Joined.map, Joined.prod, Joined.pi along the way.

Follow-up to #40092.

AI disclosure

  • level: Level 5 / Level 6 in the link shared -- I feel confident about the math but I am still learning Lean itself
  • code: most of the Lean in this PR was drafted by Claude Code (statements, proofs, docstrings).
  • direction and review: I chose the contribution, made the decisions, reviewed every line, and wrote all GitHub/Zulip comments.
  • testing: I ran local lake build of files and lake env lean of some test files (uncommitted)

@github-actions github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 12, 2026
@github-actions

github-actions Bot commented Jul 12, 2026

Copy link
Copy Markdown

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@github-actions github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jul 12, 2026
@github-actions

github-actions Bot commented Jul 12, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary a65e74ebc7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

+ Joined.map
+ Joined.pi
+ Joined.prod
+ connectedComponent_pi
+ connectedComponent_prod
+ pathComponent_pi
+ pathComponent_prod

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit a65e74e).

  • +7 new declarations
  • −0 removed declarations
+Joined.map
+Joined.pi
+Joined.prod
+connectedComponent_pi
+connectedComponent_prod
+pathComponent_pi
+pathComponent_prod

No changes to strong technical debt.

No changes to weak technical debt.

Current commit a65e74ebc7
Reference commit fd1d54bcac

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@korbonits

korbonits commented Jul 12, 2026

Copy link
Copy Markdown
Contributor Author

LLM-generated

@github-actions github-actions Bot added the LLM-generated PRs with substantial input from LLMs - review accordingly label Jul 12, 2026
@grunweg

grunweg commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

Hi! Can you update the PR description to mention how you used AI, please? Thanks.

@grunweg grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 16, 2026
@korbonits

korbonits commented Jul 17, 2026

Copy link
Copy Markdown
Contributor Author

Hi! Can you update the PR description to mention how you used AI, please? Thanks.

Done! Thanks for your review 🙏

-awaiting-author

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 17, 2026
j-loreaux
j-loreaux reviewed Aug 6, 2026
View reviewed changes

@j-loreaux j-loreaux left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors merge

@mathlib-bors mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Aug 6, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Aug 6, 2026
@korbonits
feat(Topology/Connected): connected and path components of products a…
70ee6f0 
…nd pi types (#41661)

Add `connectedComponent_prod/pi` and `pathComponent_prod/pi`: the (path) component of a point in a product is the product of the components of its coordinates. Also add the missing `Joined.map`, `Joined.prod`, `Joined.pi` along the way.
@mathlib-bors mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Aug 6, 2026
@mathlib-bors

mathlib-bors Bot commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

This PR was included in a batch that timed out, it will be automatically retried

@mathlib-bors mathlib-bors Bot removed the bors-staging This PR is currently being built by bors on the staging branch. label Aug 6, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Aug 7, 2026
@korbonits
feat(Topology/Connected): connected and path components of products a…
639a424 
…nd pi types (#41661)

Add `connectedComponent_prod/pi` and `pathComponent_prod/pi`: the (path) component of a point in a product is the product of the components of its coordinates. Also add the missing `Joined.map`, `Joined.prod`, `Joined.pi` along the way.
@mathlib-bors mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Aug 7, 2026
@mathlib-bors

mathlib-bors Bot commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(Topology/Connected): connected and path components of products and pi types [Merged by Bors] - feat(Topology/Connected): connected and path components of products and pi types Aug 7, 2026
@mathlib-bors mathlib-bors Bot closed this Aug 7, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

Assignees

@j-loreaux j-loreaux

Labels

bors-staging This PR is currently being built by bors on the staging branch. LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@korbonits @grunweg @j-loreaux